module ABSTRACT_INTERPRETER
open System
open BJK
open FSEvent

(* composition operator for context-graphs *)
let (@@) (g1 : CG.graph) (g2 : CG.graph) = CG.compose(g1,g2)

(* LUB (join) operator for context-graphs *)

let (|||) (g1 : CG.graph) (g2 : CG.graph) = CG.joinWithClonedDFRs(g1,g2)
    
(* type AbstractInterpreter encapsulates the abstract interpreter algorithm, as described in abstractInterpreterAlgorithm.docx *)
type AbstractInterpreter(analysis_params : Analysis.ANALYSIS_PARMS) =
    let Debug = ref false
     
    (* event to notify that a command's graph was updated *)      
    [<CLIEvent>]
    member x.CommandGraphUpdated = commandGraphUpdated.Publish

    [<CLIEvent>]
    member x.DebugInfoAdded = debugInfoAdded.Publish
 
    (* the entry point for the abstact interpreter execution. Recieves a command of the core language as input (in AST form) and 
       returns a context-graph which represents the algorithm analysis results on the input command. *)
    member x.analyse(c : Core.Cmd) : CG.graph =  
            (* a global identifier which is updated (at the beginning of the algorithm execution) 
           to hold the number of variables in the analysed program. *)
        let numVars = ref 0;
        (* an iterator for debug print-out which is increased on each analysis interation over a loop body. *)
        let itCount = ref 0;
        (* debug mode -  when true - each algorithm stage will be printed, along with its output (and sometimes input). *)                
        (* Sends s to the any debug info added event listener. *)
        let debugPrint(s) = if (!Debug) then debugInfoAdded.Trigger(DebugInfoAddedEventArgs(s))

        let debugPrintG(g) = if (!Debug) then debugPrint(CG.prtEdges(g))
        (* returns flow i-(1)->i if i is not in source context and i <> x *)
        let computeFlowFromItoI(c : CoreEx.Cmd, i : int, x : int, srcContext : CG.Context) =
            if (i <> x && (not (CG.inContext(i,srcContext)))) then [(i,i,D.One,CoreEx.pat(c))] else [];

        (* computes context graph for commands of the form "X := 0" *)
        let computeAsgnZeroGraph(c : CoreEx.Cmd, x : int, preContexts : CG.Context list) : CG.graph =        
            let computeDataFlows(srcContext : CG.Context) : (mat.DataFlow) list =            
                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : CG.Context) ->
                        computeFlowFromItoI(c,i,x,srcContext) @ computeMultipleFlows(i-1,srcContext);
            
                computeMultipleFlows((!numVars),srcContext)
                
                
            let computeEdge(srcContext : CG.Context) =             
                (* create target context identical to source context, at least at first... *)
                let tgtContext = CG.copyContext(srcContext);
                (* include x in target context (equivalent to assignment of X := 0) *)
                let _ = CG.addVarToContext(x,tgtContext);
                let m = mat.M(computeDataFlows(srcContext));
                  
                CG.E ( srcContext, tgtContext, ref (sop_bar.Dfr(m, mat.r(m))) )
                
            
            CG.newGraph(List.map computeEdge preContexts)
              

        (* computes context graph for commands of the form "X := Y" *)
        let computeAsgnVarGraph(c : CoreEx.Cmd, x : int, y : int, preContexts : CG.Context list) : CG.graph =       
            let computeDataFlows(srcContext : CG.Context) : (mat.DataFlow) list =          
                let computeFlowFromYtoX(i : int, srcContext : CG.Context)  =
                    if (i = y && (not (CG.inContext(y, srcContext)))) then 
                        [(y,x,D.One,CoreEx.pat(c))]
                    else 
                        [];
              
                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : CG.Context) ->                
                            let flowYtoX = computeFlowFromYtoX(i,srcContext);
                            let flowItoI = computeFlowFromItoI(c,i,x,srcContext);
                            flowYtoX @ flowItoI @ computeMultipleFlows(i-1, srcContext)
                       
                computeMultipleFlows((!numVars), srcContext)
               
                
            let computeEdge(srcContext : CG.Context) =            
                (* create target context identical to source context, at least at first... *)
                let tgtContext = CG.copyContext(srcContext);
                let y_in_srcContext = CG.inContext(y, srcContext);
                (* add x to target context if y is in source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y, where Y <> 0) *)
                let () = CG.setVarInContext(x, tgtContext, y_in_srcContext); 
                let m = mat.M(computeDataFlows(srcContext));
            
                CG.E ( srcContext, tgtContext, ref (sop_bar.Dfr(m, [])) )
        
            CG.newGraph(List.map computeEdge preContexts)
               

        (* computes context graph for commands of the form "X := Y * Z" *)
        let computeAsgnTimesGraph(c : CoreEx.Cmd, x, y, z, preContexts) : CG.graph =         
            let computeDataFlows(srcContext : CG.Context) : (mat.DataFlow) list =            
                let computeSingleFlow(i : int, srcContext : CG.Context) : (mat.DataFlow) list =                
                    (* add flow y-(2)->x (or z-(2)->x) if y and z are both not in the source context (equivalent to assignment of X := Y*Z where Y>0 and Z>0 ) *)
                    let computeFlowFromYandZtoX(i : int, srcContext : CG.Context) =
                        if ( (i = y || i = z) &&
                             (not (CG.inContext(y, srcContext) || CG.inContext(z, srcContext))) )
                        then [(i,x,analysis_params.nonlinear_Dvalue,CoreEx.pat(c))]
                        else [];
                
                    computeFlowFromYandZtoX(i,srcContext) @ computeFlowFromItoI(c,i,x,srcContext)
                
                let rec computeMultipleFlows = function 
                    | (0,_) -> []
                    | (i : int, srcContext : CG.Context) ->
                        computeSingleFlow(i, srcContext) @ computeMultipleFlows(i-1, srcContext);
            
                computeMultipleFlows((!numVars), srcContext)
                
            let computeEdge(srcContext : CG.Context) =            
                (* create target context identical to source context, at least at first... *)
                let tgtContext = CG.copyContext(srcContext);
                let y_or_z_in_srcContext = (CG.inContext(y, srcContext)) || (CG.inContext(z, srcContext));
                (* add x to target context if  y or z are in the source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y * Z, where Y>0 and Z > 0) *)
                let _ = CG.setVarInContext(x, tgtContext, y_or_z_in_srcContext); 
                let mat = mat.M(computeDataFlows(srcContext));
            
                CG.E ( srcContext, tgtContext, ref (sop_bar.Dfr(mat, [])) )
        
            CG.newGraph( List.map computeEdge preContexts )    

        (* computes context graph for commands of the form "X := Y + Z" *)    
        let computeAsgnPlusGraph(c : CoreEx.Cmd, x, y, z, preContexts) : CG.graph =        
            let computeDataFlows(x : int, y : int, z : int, srcContext : CG.Context) : (mat.DataFlow) list =            
                let computeSingleFlow(i : int, srcContext : CG.Context) : (mat.DataFlow) list =               
                    (* add flow y-(1')->x (or z-(1')->x) if y (or z) are not in the source context (equivalent to assignment of X := Y+Z where Y>0 or Z>0 ) *)
                    let computeFlowFromYandZtoX(i : int, srcContext : CG.Context) =                   
                        let iNotInSrcContext = not (CG.inContext(i,srcContext))
                        let yInSrcContext = CG.inContext(y, srcContext)
                        let zInSrcContext = CG.inContext(z, srcContext)
                    
                        if (i = y || i = z) then
                            if (iNotInSrcContext && (not (yInSrcContext && zInSrcContext))) then 
                                if ((not yInSrcContext) && (not zInSrcContext)) then
                                    if y = z then
                                        [(i,x,D.Two,CoreEx.pat(c))] (* when the same var is added then we deduce polynomial growth *)
                                    else
                                        [(i,x,D.One',CoreEx.pat(c))]
                                else 
                                    [(i,x,D.One,CoreEx.pat(c))]
                            else []
                        else []
             
                    computeFlowFromYandZtoX(i,srcContext) @ computeFlowFromItoI(c,i,x,srcContext)
                
                let rec computeMultipleFlows = function
                    | (0,_) -> []
                    | (i : int, srcContext : CG.Context) ->
                            computeSingleFlow(i,srcContext) @ computeMultipleFlows(i-1,srcContext);                                  
            
                computeMultipleFlows((!numVars),srcContext)
                
            let computeEdge(srcContext : CG.Context) =          
                (* create target context identical to source context, at least at first... *)
                let tgtContext = CG.copyContext(srcContext);
                let y_and_z_in_srcContext = (CG.inContext(y, srcContext)) && (CG.inContext(z, srcContext));
                (* add x to target context if  y and z are both in the source context (equivalent to assignment of X := 0),
                    otherwise exclude x from target context (equivalent to assignment of X := Y + Z, where Y>0 or Z > 0) *)
                let _ = CG.setVarInContext(x, tgtContext, y_and_z_in_srcContext);  
                let m = mat.M(computeDataFlows(x,y,z,srcContext));
            
                CG.E ( srcContext, tgtContext, ref (sop_bar.Dfr(m, mat.r(m))) )        
        
            CG.newGraph( List.map computeEdge preContexts )


        (* updates DFRs on all edges of graph g with all possible data flows of the form (i->j,i'->j'). *)
        let computeDoubleFlows(g : CG.graph) =       
            let updateDoubleFlowsOnEdge = function
                | ( CG.E(p, q, refDfr) ) ->  
                    (* filter letction to determine if a given double data flow should be included in the result *)
                    let includeFlow (p : CG.Context,q : CG.Context) ((i,j),(i',j'),pat) = 
                                    (not (CG.inContext(i,p))) && (not (CG.inContext(i',p))) &&
                                    (not (CG.inContext(j,q))) && (not (CG.inContext(j',q))) &&
                                    (i <> i' || j <> j');
                    match !refDfr with
                    | (sop_bar.Dfr(m,_)) as dfr ->           
                            (* filter double flows according to source and target contexts *)
                            let r' = List.filter (includeFlow(p,q)) (mat.r(m));                        
                            refDfr := sop_bar.Dfr(m,r')
                | _ ->  Util.fail("AbstractInterpreter.updateDoubleFlowsOnEdge: Invalid argument.")     
     
     
            List.iter updateDoubleFlowsOnEdge (CG.edges(g))

        (* computes a graph corresponding to the abstract interpretation of an assignment command, with given pre-contexts *)
        let computeAssignmentGraph (c : CoreEx.Cmd, x : int, e : Core.Expr, preContexts : CG.Context list) : CG.graph ref =
            (* computes data flows of the form i-(d)->j *)
            let computeSingleFlows (x : int, e : Core.Expr, preContexts : CG.Context list) : CG.graph =
                match e with
                | Core.Zero ->                          computeAsgnZeroGraph(c, x, preContexts)
                | Core.Var y ->                          computeAsgnVarGraph(c,x, y, preContexts)
                | Core.Times(Core.Var y, Core.Var z) -> computeAsgnTimesGraph(c, x, y, z, preContexts)                                      
                | Core.Plus(Core.Var y , Core.Var z) -> computeAsgnPlusGraph(c, x, y, z, preContexts);
                | _ -> Util.fail("AbstractInterpreter.computeAssignmentGraph: Invalid argument.")
            
            let g' = ref (computeSingleFlows(x, e, preContexts));
            (* computes all data flows of the form (i->j,i'->j') over the flows calculated for all edges of the graph g' *)
            let () = computeDoubleFlows(!g');
            g'
             
        (* abstractly interpret command c,  creating (or updating) its CG.graph, return ref to resulting graph *)
        let rec abstractInterpret(c : CoreEx.Cmd, preContexts : CG.Context list) : CG.graph ref =       
            (* Computes the loop correction on all edges where applicable. This letction applies loop rule L2 in the DICE paper. *)
            let doLoopCorrection(l : int, g : CG.graph ref)  =          
                (* overload operator * to represent DFR composition, in thie scope of this letction only *)
                let (*) (d1 : sop_bar.DFR) (d2 : sop_bar.DFR) : sop_bar.DFR = sop_bar.prod(d1,d2)
                                                
                (* The loop correction operator on DFRs. *)
                let LC(l,sop_bar.Dfr(m,r)) =               
                    let m' = mat.LC (l, analysis_params.nonlinear_Dvalue, CoreEx.id(c)) m;            
                    sop_bar.Dfr(m', sop_bar.filterR(r,m'))
                
                for p in (!g).Keys do
                    for qd in (!g).[p] do
                        let q = qd.Key
                        for p' in (!g).Keys do
                            for qd' in (!g).[p'] do
                               let q' = qd'.Key
                               if (CG.eqContexts(q,p')) then
                                   match CG.getEdgeTag(!g,CG.UE (q,q)) with
                                              | Some (dfr) -> 
                                                            let d = qd.Value
                                                            let d' = qd'.Value
                                                            CG.addEdge(!g, CG.E (p,q', ref ( !d * LC(l, !dfr) * !d' )), false) 
                                                            (*compute the loop correction where applicable *)
                                              | None     -> ()
            
            (* computes result graph of a single loop iteration, provided that the loop body is c and
               that execution of all loop iterations so far have resulted with the graph g. *)
            let doSingleIteration (g : CG.graph ref, c : CoreEx.Cmd)  =            
                let () = debugPrint("=======doSingleIteration=========\nIteration #"  + (!itCount).ToString() + ":\n");
                (* Compute the graph representing the loop body, with pre-contexts which are the post contexts of the current gaph.
                   This is a graph which represents the next iteration of the loop. *)
                let g' = abstractInterpret(c, CG.postContexts(!g));
                let () = debugPrint("current graph(g):\n");
                let () = debugPrintG(!g);
                let () = debugPrint("graph to compose(g'):\n");
                let () = debugPrintG(!g');
                (* now, compute the composition of current iteration and the next iteration graphs *)
                let g'' = !g @@ !g';
                let () = debugPrint("composed graph(g''):\n")
                let () = debugPrintG(g'');
                (* now - join the results of last iteration with results of current iteration,
                   and the composition of last result with current iteration *)
                let g''' = !g ||| !g' ||| g'';
                let () = debugPrint("join result graph(g'''):\n");
                let () = debugPrintG(g''');
                let () = debugPrint("================================\n");
                let () = itCount := !itCount + 1;           
                (* return the result graph representing the next loop iteration *)
                g'''


            (* Compute the result graph of any m >0 iterations of the loop whose body is c and the iterator variable is x.
               Update the result graph to g. This letction applies loop rule L1 in the DICE paper. *)
            let doLoopClosure(x : int, c : CoreEx.Cmd, g : CG.graph ref) : CG.graph ref =           
                (* least fixed point letction *)
                let rec lfp f (g : CG.graph ref, c : CoreEx.Cmd) : CG.graph ref =                 
                    let () = debugPrint("lfp: g before:\n")
                    let () = debugPrintG(!g);
                    let fg = f(g, c);
                    let isEq = CG.equal(fg,!g);
                    let () = debugPrint(if (isEq) then "lfp reached!\n" else "lfp not reached!\ng:\n");
                    let () = debugPrintG(!g);
                    let () = debugPrint("fg:\n");
                    let () = debugPrintG(fg);
                
                    if (isEq) then g else (g := fg; 
                                           debugPrint("lfp: g after:\n");
                                           debugPrintG(!g);
                                           lfp f (g,c))

                let () = itCount := 0;
            
                lfp doSingleIteration (g,c)
            
            (* Splits the context list into 2 seperate lists, the first list contains all contexts
               which include the variable var and the second list will contain all contexts which
               do not include the vairable var. *)   
            let rec splitContextListAccordingToVarInclusion(contextList : CG.Context list, var : int) =
                 match contextList with
                 |  []      ->  ([],[])
                 |  c::cl   ->  let (included,notIncl) = splitContextListAccordingToVarInclusion(cl, var)
                                let inContext = CG.inContext(var,c) 
                                let c' = (if inContext then c::included else included)
                                let c'' = (if inContext then notIncl else c::notIncl)
                                (c',c'')
                   
            (* apply the loop rules. The result graph is updated in g *)
            let doLoop(x : int, c : CoreEx.Cmd, preContexts : CG.Context list, g : CG.graph ref) : CG.graph ref =           
                (* Sort precontexts into 2 lists: incl - contexts which include x
                                                  notIncl - contexts which don't include x *)
                let (incl,notIncl) = splitContextListAccordingToVarInclusion(preContexts, x)
                
                (* Compute graph for skip command given incl precontexts.
                   This graph represent the case where the loop iterator is zero *)
                let skipGraph = computeAssignmentGraph(c, 1,Core.Var 1, incl)
                
                (* when there are no pre-contexts, this means that in all
                   possible conditions, the loop bounding variable is zero, 
                   hence the loop has no effect. *)
                if List.isEmpty(notIncl) then
                    let () = g := !skipGraph 
                    g

                else
                    (* compute graph representing loop's body, including a possibility of zero iterations (skip).
                        This action also applies loop rule L0 in the DICE paper 
                        (since each loop body c was expanded to "if { Skip } else { c }").*)
                    let () = g := !(abstractInterpret(c, notIncl))
                    (* compute graph representing any m>0 iterations of the loop body *)
                    let _ = doLoopClosure(x, c, g) 
                    let () = debugPrint("after loop closure.\n");
                    let () = commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c,!g,""))
                    let () = doLoopCorrection(x, g)
                    let () = debugPrint("after loop correction.\n");
                    let () = commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c,!g,""))
                    let () = CG.filterEdgesByPreContexts(g, notIncl) 
                    let () = debugPrint("after edge filtering.\n");
                    let () = commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c,!g,""))
                    let () = g := !g ||| !skipGraph
                    g
            
                    

            
            (* computes the composition result graph of commands c1 and c2 and updates it to g *)
            let doCompose(c1 : CoreEx.Cmd,c2 : CoreEx.Cmd, preContexts : CG.Context list, g : CG.graph ref) : CG.graph ref =                   
                let g1 = abstractInterpret(c1, preContexts);
                let g2 = abstractInterpret(c2, (CG.postContexts(!g1)));
                let () = g := (!g1 @@ !g2);                                        
                g


            (* computes the join(Least Upper Bound) result graph of commands c1 and c2 and updates it to g *)            
            let doChoice(c1 : CoreEx.Cmd,c2 : CoreEx.Cmd, preContexts : CG.Context list, g : CG.graph ref) : CG.graph ref =            
                let () = g := (!(abstractInterpret(c1, preContexts)) ||| !(abstractInterpret(c2, preContexts)))        
                g
                
                
            (* the actual interpreter step - recursively interpret the command according to it's type and update it's attached graph with the result. *)            
            let internalInterpret(CoreEx.AICmd(c,g,_) as c': CoreEx.Cmd, preContexts : CG.Context list) : CG.graph ref =
                let g = match c with 
                        |  CoreEx.Seq(c1,c2)        -> doCompose(c1,c2,preContexts, g)
                        |  CoreEx.Choice(c1,c2)     -> doChoice(c1,c2,preContexts,g)
                        |  CoreEx.Skip              -> computeAssignmentGraph(c', 1,Core.Var 1, preContexts)
                        |  CoreEx.Asgn(i, e)        -> computeAssignmentGraph(c', i, e, preContexts)
                        |  CoreEx.Loop(i, c)        -> doLoop(i,c,preContexts,g);
                (* send event that command graph was updated *)
                commandGraphUpdated.Trigger(CommandGraphUpdatedEventArgs(c',!g,""))
                g
                

            (* returns true if command c must be re-interpreted. This will be so if current pre-contexts are 
               not a sub-set of the pre-contexts of the graph attached to command c *)
            let shouldUpdateCommandGraph(c,preContexts) =          
                let g = CoreEx.graph(c);      
                not (CG.preContextsIn(preContexts,!g))

            
            (* get reference to graph attached to command c *)
            let g = CoreEx.graph(c);
            let () = debugPrint("Started analysing command:\n");
            let () = debugPrint(CoreEx.prt(c));
            let () = if (shouldUpdateCommandGraph(c,preContexts)) then 
                        g := !(internalInterpret(c, preContexts))
                        
                     else (); (* if graph doesn't need to be updated - do nothing *)
            let () = debugPrint("Finished analysing command:\n" + CoreEx.prt(c) + "result graph:\n");
            let () = debugPrintG(!g);
            let () = debugPrint("============================================\n");
        
            g
      
        (* initialize "global" identifier. *)
        let () = (numVars := Core.highest_var(c));
        (* Attach a context graph to each command, and convert each loop body c to "if { Skip} else { c }". *)
        let c' = CoreEx.extendedAbsIntAST(c);
    
        (* start running the abstract interpreter with a pre-contexts list containing only the empty context, 
           since at first we assume no contexts. *)
        !(abstractInterpret(c',[CG.makeEmptyContext(!numVars)]))

    member x.resultText(c, g : CG.graph) =
        let vars = Core.highest_var c 
        let bounded = ref [1..vars]
        let vt = BJKParse.parserLastVarToIndexMap()
        
        let rec prt_ints  = function
            | [] -> "\n"
            | i::rest -> let varFound = vt.ContainsKey(i)
                         (if varFound then vt.[i] else "") + (if varFound && rest<>[] then ", " + (prt_ints rest) else "\n")
       
        let removeNonBounded(b, nb) = 
            List.filter (fun x -> not (List.exists (fun y -> x=y) nb)) b
              
        for p in g.Keys do
            for et in g.[p].Values do  
                match !et with
                    | (sop_bar.Dfr(M,_)) ->
                            let (notbounded', _) = mat.classify(M,vars)
                            bounded := removeNonBounded(!bounded, notbounded')
        let nonbounded = List.filter (fun v -> not (List.exists (fun v' -> v'=v) !bounded)) [1..vars]            
        ("\n\nVARS: " + (vars.ToString()) + "\n" + analysis_params.name + ": " +
                 (prt_ints !bounded) + ("NON-" + analysis_params.name + ": ") + (prt_ints nonbounded)) 
    
    (* set the debug output mode *)
    member x.setDebugMode(mode : bool) = Debug := mode

(* type AbstractInterpreter *)

let Poly = AbstractInterpreter(Analysis.PolyParams())        

let Lin = AbstractInterpreter(Analysis.LinParams())        




